\section{Prerekvizity a označenia}

V tejto časti si zhrnieme najdôležitejšie označenia, pojmy a vety z
prednášky ``Úvod do matematickej logiky''.

\noindent Označenia:
\begin{itemize}
    \item $\provable A$ -- formula $A$ je dokázateľná
    \item $\mathcal{M} \models A$ -- $\mathcal{M}$ je modelom $A$
    \item $\implies, \lequiv$ -- implikácia, ekvivalencia vo
    výrokovej/predikátovej logike
    \item $\Rightarrow, \Leftrightarrow$ -- implikácia a ekvivalencia v
    našom jazyku
\end{itemize}

\noindent Axiómy:
\begin{itemize}
    \item[A1:] $A \implies (B \implies A)$
    \item[A2:] $(A \implies (B \implies C)) \implies 
                [(A \implies B) \implies (A \implies C)]$
    \item[A3:] $(\neg B \implies \neg A) \implies (A \implies B)$
    \smallskip
    \item[A4:] $(\forall x) A \implies A_x[t]$
    \item[A5:] $(\forall x) (A \implies B) \implies (A \implies
    (\forall x) B)\quad$ (ak $x$ nie je voľná v $A$)
\end{itemize}

\noindent Pravidlá:
\begin{itemize}
    \item Modus ponens: $\displaystyle \frac{A,A\implies B}{B}$
    \item Pravidlo zovšeobecnenia:
            $\displaystyle \frac{A,x}{(\forall x)A}$
    \item Jednoduchý sylogizmus:
            $\displaystyle \frac{A, A\implies B, B\implies C}{C}$, resp.
            $\provable (A \implies B) \implies ((B \implies C) 
                \implies (A \implies C))$.
\end{itemize}

\begin{veta}[O dedukcii]
    \begin{equation*}
        T \provable A \implies B \iff T,A \provable B
    \end{equation*}
    Pozn.: V predikátovej logike ale musí na implikáciu $\Leftarrow$ 
    navyše platiť, že na žiadnu voľnú premennú z formly $A$
    nepoužijeme v dôkaze $T,A \provable B$ pravidlo zovšeobecnenia.
    Špeciálne teda ekvivalencia platí v prípade, že $A$ je uzavretá.
\end{veta}

\begin{veta}[Postove vety a iné užitočné tvrdenia]
    \noindent
    \begin{itemize}
        \item $\provable A \implies A$
        \item $\provable A \implies \neg \neg A$
        \item $\provable \neg \neg A \implies A$
        \item $\provable (A \implies B) \implies (\neg B \implies \neg A)$
    \end{itemize}
\end{veta}

\begin{lema}[O neutrálnej formule]
   Nech $T,A \provable B$ a tiež $T, \neg A \provable B$. Potom
   $T \provable B$.
\end{lema}

\begin{lema}[O distribúcii kvantifikátorov]
    Ak je $\provable A \implies B$, potom
    $\provable (\forall x)A \implies (\forall x) B$ a
    $\provable (\exists x)A \implies (\exists x)B$.
\end{lema}

\begin{veta}[O ekvivalencii]
    Nech formula $A'$ vznikne z formuly A nahradením všetkých výskytov 
    podformúl $B_1,\dots ,B_n$ v uvedenom poradí formulami 
    $B'_1, \dots, B'_n$. Ak platí $\provable B_i \lequiv B'_i$ pre
    $i \in \{1,\dots,n\}$, potom $\provable A \lequiv A'$.
\end{veta}

\todo{vety o variantoch, zavedeni kvantifikatorov, ...}
\begin{lema}[Duálny tvar axiómy špecifikácie]
    $\provable A_x[t] \implies (\exists x) A$
\end{lema}

\begin{lema}[Pravidlo zavedenia existenčného kvantifikátora]
    Ak $\provable A \implies B$ a $x$ nie je voľná v $B$, potom
    $\provable (\exists x) A \implies B$.
\end{lema}
